($\lambda$$T$,${\it as}$,${\it bs}$,$z$. ${\it as}$ @ ${\it bs}$) $\in$ $T$:Type$\rightarrow$($T$ List)$\rightarrow$($T$ List)$\rightarrow\downarrow$True$\rightarrow$($T$ List)